Nuprl Lemma : test-eq-E-update
11,40
postcript
pdf
es
:ES,
e
:E.
e
=
e
latex
Definitions
s
=
t
,
t
T
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
ES
,
E
,
b
,
strong-subtype(
A
;
B
)
,
P
Q
,
P
Q
,
x
:
A
B
(
x
)
,
P
&
Q
,
P
Q
,
A
,
e
=
e'
,
b
,
p
q
,
p
q
,
p
q
Lemmas
assert-es-eq-E-2
,
assert
wf
,
es-E
wf
,
event
system
wf
origin
es:ES, e:E. 
e = e es:ES, e:E. e = e 
T
B(x)x:A. B(x)b
Q
Q
B(x) Q
A
b q
q
q